$\forall$$g$, $h$:GrpSig, $f$:MonHom($g$,$h$).
\\[0ex]fun\_thru\_1op($\mid$$g$$\mid$;$\mid$$h$$\mid$;$\sim$;$\sim$;$f$) $\Rightarrow$ Inj($\mid$$g$$\mid$;$\mid$$h$$\mid$;$f$) $\Rightarrow$ Inverse($\mid$$h$$\mid$;$\ast$;e;$\sim$) $\Rightarrow$ Inverse($\mid$$g$$\mid$;$\ast$;e;$\sim$)